$\forall$$A$,$B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$). proddeq($a$; $b$) $\in$ (:$A$ $\times$ $B$)$\rightarrow$(:$A$ $\times$ $B$)$\rightarrow\mathbb{B}$